{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Introduction"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this notebook, we will demonstrate some of the differences between SymPy's `logic` module, and PyEDA's logic expressions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "import sympy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "import pyeda.boolalg.expr\n",
    "import pyeda.boolalg.bfarray"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Create Variables"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `xs` array is a tuple of SymPy symbolic variables,\n",
    "and the `ys` array is a PyEDA function array."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "xs = sympy.symbols(\",\".join(\"x%d\" % i for i in range(64)))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "ys = pyeda.boolalg.bfarray.exprvars('y', 64)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Basic Boolean Functions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Create a SymPy XOR function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "f = sympy.Xor(*xs[:4])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Create a PyEDA `XOR` function:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "g = pyeda.boolalg.expr.Xor(*ys[:4])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "SymPy `atoms` method is similar to PyEDA's `support` property:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "f.atoms()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "g.support"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "SymPy's `subs` method is similar to PyEDA's `restrict` method:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "f.subs({xs[0]: 0, xs[1]: 1})"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "g.restrict({ys[0]: 0, ys[1]: 1})"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Conversion to NNF"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Conversion to negation normal form is also similar. One difference is that SymPy inverts the variables by applying a `Not` operator, but PyEDA converts inverted variables to *complements* (a negative *literal*)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "sympy.to_nnf(f)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "type(sympy.Not(xs[0]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "g.to_nnf()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "type(~ys[0])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Conversion to DNF"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Conversion to disjunctive normal form, on the other hand, has some differences. With only four input variables, `SymPy` takes a couple seconds to do the calculation. The output is large, with unsimplified values and redundant clauses."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "sympy.to_dnf(f)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "PyEDA's DNF conversion is minimal:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "g.to_dnf()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "It's a little hard to do an apples-to-apples comparison, because 1) SymPy is pure Python and 2) the algorithms are probably different.\n",
    "\n",
    "The `simplify_logic` function actually looks better for comparison:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "from sympy.logic import simplify_logic"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "simplify_logic(f)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "simplify_logic(f)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Running this experiment from `N=2` to `N=6` shows that PyEDA's runtime grows significantly slower."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "import numpy as np\n",
    "import matplotlib.pyplot as plt"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": [
    "%matplotlib inline"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "N = 5\n",
    "\n",
    "sympy_times = (.000485,  .000957, .00202,  .00426, .0103)\n",
    "pyeda_times = (.0000609, .000104, .000147, .00027, .000451)\n",
    "\n",
    "ind = np.arange(N)  # the x locations for the groups\n",
    "width = 0.35        # the width of the bars\n",
    "\n",
    "fig, ax = plt.subplots()\n",
    "\n",
    "rects1 = ax.bar(ind, sympy_times, width, color='r')\n",
    "rects2 = ax.bar(ind + width, pyeda_times, width, color='y')\n",
    "\n",
    "# add some text for labels, title and axes ticks\n",
    "ax.set_ylabel('Time (s)')\n",
    "ax.set_title('SymPy vs. PyEDA: Xor(x[0], x[1], ..., x[n-1]) to DNF')\n",
    "ax.set_xticks(ind + width)\n",
    "ax.set_xticklabels(('N=2', 'N=3', 'N=4', 'N=5', 'N=6'))\n",
    "\n",
    "ax.legend((rects1[0], rects2[0]), ('SymPy', 'PyEDA'))\n",
    "\n",
    "plt.show()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Going a bit further, things get worse.\n",
    "\n",
    "These numbers are from my laptop:\n",
    "\n",
    "|  N | sympy    | pyeda    | ratio  |\n",
    "|----|----------|----------|--------|\n",
    "|  2 |  .000485 | .0000609 |   7.96 |\n",
    "|  3 |  .000957 | .000104  |   9.20 |\n",
    "|  4 |  .00202  | .000147  |  13.74 |\n",
    "|  5 |  .00426  | .00027   |  15.78 |\n",
    "|  6 |  .0103   | .000451  |  22.84 |\n",
    "|  7 |  .0231   | .000761  |  30.35 |\n",
    "|  8 |  .0623   | .00144   |  43.26 |\n",
    "|  9 |  .162    | .00389   |  41.65 |\n",
    "| 10 |  .565    | .00477   | 118.45 |\n",
    "| 11 | 1.78     | .012     | 148.33 |\n",
    "| 12 | 6.46     | .0309    | 209.06 |"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Simplification"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "SymPy supports some obvious simplifications, but PyEDA supports more. Here are a few examples."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "sympy.Equivalent(xs[0], xs[1], 0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "pyeda.boolalg.expr.Equal(ys[0], ys[1], 0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "sympy.ITE(xs[0], 0, xs[1])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "pyeda.boolalg.expr.ITE(ys[0], 0, ys[1])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "sympy.Or(xs[0], sympy.Or(xs[1], xs[2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "pyeda.boolalg.expr.Or(ys[0], pyeda.boolalg.expr.Or(ys[1], ys[2]))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "sympy.Xor(xs[0], sympy.Not(sympy.Xor(xs[1], xs[2])))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "pyeda.boolalg.expr.Xor(ys[0], pyeda.boolalg.expr.Xnor(ys[1], ys[2]))"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.4.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}
